Recent Challenges and Ideas in Temporal Synthesis
Identifieur interne : 000232 ( Main/Exploration ); précédent : 000231; suivant : 000233Recent Challenges and Ideas in Temporal Synthesis
Auteurs : Orna Kupferman [Israël]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2012.
English descriptors
- Teeft :
- Algorithm, Algorithmic, Algorithmic game theory, Atomic propositions, Automatic synthesis, Automaton, Boolean, Computer science, Correct system, Current synthesis algorithms, Current theory, Determinization, Determinization construction, Different aspects, Formalism, Genetic programming, Heidelberg, Ieee symp, Kupferman, Lncs, Logic formula, Nite, Nonemptiness, Output signals, Parity, Parity games, Pnueli, Possible environments, Probabilistic components, Proc, Programming languages, Quantitative properties, Rational synthesis, Reactive, Reactive systems, Real life, Realizability, Realizability problem, Recent challenges, Reusable components, Ronchi della rocca, Solution concept, Springer, State space, Symp, Synthesis, Synthesis algorithm, Synthesis algorithms, Synthesis problem, System synthesis, Temporal, Temporal assertions, Temporal logic, Temporal synthesis, Theoretical computer science, Traditional algorithm, Tree automata, Vardi, Weak synthesis.
Abstract
Abstract: In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification against all environments. While model-checking theory has led to industrial development and use of formal-verification tools, the integration of synthesis in the industry is slow. This has to do with theoretical limitations, like the complexity of the problem, algorithmic limitations, like the need to determinize automata on infinite words and solve parity games, methodological reasons, like the lack of satisfactory compositional synthesis algorithms, and practical reasons: current algorithms produce systems that satisfy the specification, but may do so in a peculiar way and may be larger or less well-structured than systems constructed manually. The research community has managed to suggest some solutions to these limitations, and bring synthesis algorithms closer to practice. Significant barriers, however, remain. Moreover, the integration of synthesis in real applications has taught us that the traditional setting of synthesis is too simplified and has brought with it new algorithmic challenges. This paper introduces the synthesis problem, algorithms for solving it, and recent promising ideas in making temporal-synthesis useful in practice.
Url:
DOI: 10.1007/978-3-642-27660-6_8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000B20
- to stream Istex, to step Curation: 000A64
- to stream Istex, to step Checkpoint: 000102
- to stream Main, to step Merge: 000232
- to stream Main, to step Curation: 000232
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Recent Challenges and Ideas in Temporal Synthesis</title>
<author><name sortKey="Kupferman, Orna" sort="Kupferman, Orna" uniqKey="Kupferman O" first="Orna" last="Kupferman">Orna Kupferman</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:699C928CD9F894B5D63A22D7D39A5C8185799EF1</idno>
<date when="2012" year="2012">2012</date>
<idno type="doi">10.1007/978-3-642-27660-6_8</idno>
<idno type="url">https://api.istex.fr/document/699C928CD9F894B5D63A22D7D39A5C8185799EF1/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000B20</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000B20</idno>
<idno type="wicri:Area/Istex/Curation">000A64</idno>
<idno type="wicri:Area/Istex/Checkpoint">000102</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000102</idno>
<idno type="wicri:doubleKey">0302-9743:2012:Kupferman O:recent:challenges:and</idno>
<idno type="wicri:Area/Main/Merge">000232</idno>
<idno type="wicri:Area/Main/Curation">000232</idno>
<idno type="wicri:Area/Main/Exploration">000232</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Recent Challenges and Ideas in Temporal Synthesis</title>
<author><name sortKey="Kupferman, Orna" sort="Kupferman, Orna" uniqKey="Kupferman O" first="Orna" last="Kupferman">Orna Kupferman</name>
<affiliation wicri:level="1"><country xml:lang="fr">Israël</country>
<wicri:regionArea>School of Engineering and Computer Science, Hebrew University, 91904, Jerusalem</wicri:regionArea>
<wicri:noRegion>Jerusalem</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Israël</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s">Lecture Notes in Computer Science</title>
<imprint><date>2012</date>
</imprint>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term>
<term>Algorithmic</term>
<term>Algorithmic game theory</term>
<term>Atomic propositions</term>
<term>Automatic synthesis</term>
<term>Automaton</term>
<term>Boolean</term>
<term>Computer science</term>
<term>Correct system</term>
<term>Current synthesis algorithms</term>
<term>Current theory</term>
<term>Determinization</term>
<term>Determinization construction</term>
<term>Different aspects</term>
<term>Formalism</term>
<term>Genetic programming</term>
<term>Heidelberg</term>
<term>Ieee symp</term>
<term>Kupferman</term>
<term>Lncs</term>
<term>Logic formula</term>
<term>Nite</term>
<term>Nonemptiness</term>
<term>Output signals</term>
<term>Parity</term>
<term>Parity games</term>
<term>Pnueli</term>
<term>Possible environments</term>
<term>Probabilistic components</term>
<term>Proc</term>
<term>Programming languages</term>
<term>Quantitative properties</term>
<term>Rational synthesis</term>
<term>Reactive</term>
<term>Reactive systems</term>
<term>Real life</term>
<term>Realizability</term>
<term>Realizability problem</term>
<term>Recent challenges</term>
<term>Reusable components</term>
<term>Ronchi della rocca</term>
<term>Solution concept</term>
<term>Springer</term>
<term>State space</term>
<term>Symp</term>
<term>Synthesis</term>
<term>Synthesis algorithm</term>
<term>Synthesis algorithms</term>
<term>Synthesis problem</term>
<term>System synthesis</term>
<term>Temporal</term>
<term>Temporal assertions</term>
<term>Temporal logic</term>
<term>Temporal synthesis</term>
<term>Theoretical computer science</term>
<term>Traditional algorithm</term>
<term>Tree automata</term>
<term>Vardi</term>
<term>Weak synthesis</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: In automated synthesis, we transform a specification into a system that is guaranteed to satisfy the specification against all environments. While model-checking theory has led to industrial development and use of formal-verification tools, the integration of synthesis in the industry is slow. This has to do with theoretical limitations, like the complexity of the problem, algorithmic limitations, like the need to determinize automata on infinite words and solve parity games, methodological reasons, like the lack of satisfactory compositional synthesis algorithms, and practical reasons: current algorithms produce systems that satisfy the specification, but may do so in a peculiar way and may be larger or less well-structured than systems constructed manually. The research community has managed to suggest some solutions to these limitations, and bring synthesis algorithms closer to practice. Significant barriers, however, remain. Moreover, the integration of synthesis in real applications has taught us that the traditional setting of synthesis is too simplified and has brought with it new algorithmic challenges. This paper introduces the synthesis problem, algorithms for solving it, and recent promising ideas in making temporal-synthesis useful in practice.</div>
</front>
</TEI>
<affiliations><list><country><li>Israël</li>
</country>
</list>
<tree><country name="Israël"><noRegion><name sortKey="Kupferman, Orna" sort="Kupferman, Orna" uniqKey="Kupferman O" first="Orna" last="Kupferman">Orna Kupferman</name>
</noRegion>
<name sortKey="Kupferman, Orna" sort="Kupferman, Orna" uniqKey="Kupferman O" first="Orna" last="Kupferman">Orna Kupferman</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Sarre/explor/MusicSarreV3/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000232 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000232 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Sarre |area= MusicSarreV3 |flux= Main |étape= Exploration |type= RBID |clé= ISTEX:699C928CD9F894B5D63A22D7D39A5C8185799EF1 |texte= Recent Challenges and Ideas in Temporal Synthesis }}
This area was generated with Dilib version V0.6.33. |